﻿using System;
using System.Collections.Generic;
using System.Text;
using DySy.Framework;
using Microsoft.Pex.Framework;

namespace DySy.Examples
{
    [PexClass(typeof(Program))]
    [DySyAnalysis]
    public class Program
    {
        /// <summary>
        /// Simple example method. We want to infer its pre-
        /// and postcondition.
        /// </summary>
        public int Foo(int a)
        {
            if (a <= 0)
                return 0;

            int b = a + 3;
            return 2 * b;
        }


        /// <summary>
        /// Existing test case. DySy will summarize its execution in terms of 
        /// pre- and post-conditions.
        /// </summary>
        [PexMethod]
        public void Entry()
        {
            Foo(1);
            Foo(10);
        }
    }
}
